i:Id, k:Knd, da:Decl, din:InDecl(i). Valtype(k;da;din)  Type 

latex

Definitions	Valtype(k;da;din), kindcase(k; a.f(a); l,t.g(l;t) ), x. t(x), x,y. t(x;y), d(a), d(p), IdLnk, InDecl(i), x:A. B(x), Decl, Knd, t  T, Id
Lemmas	Id wf, Knd wf, s-decl wf, in-decl wf, IdLnk wf, s-in-declared wf, s-declared wf, kindcase wf